$\forall$$T$:Type, ${\it as}$,${\it bs}$:($T$ List), $i$:int\_seg($\parallel$${\it as}$$\parallel$; ($\parallel$${\it as}$$\parallel$ + $\parallel$${\it bs}$$\parallel$)).
\\[0ex]append(${\it as}$; ${\it bs}$)[$i$] = ${\it bs}$[($i$ {-} $\parallel$${\it as}$$\parallel$)] $\in$ $T$